p(s(x)) → x
s(p(x)) → x
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
↳ QTRS
↳ DependencyPairsProof
p(s(x)) → x
s(p(x)) → x
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
+1(p(x), y) → +1(x, y)
+1(p(x), y) → P(+(x, y))
+1(s(x), y) → S(+(x, y))
*1(p(x), y) → +1(*(x, y), minus(y))
MINUS(p(x)) → MINUS(x)
*1(p(x), y) → *1(x, y)
MINUS(s(x)) → MINUS(x)
*1(s(x), y) → +1(*(x, y), y)
MINUS(s(x)) → P(minus(x))
+1(s(x), y) → +1(x, y)
MINUS(p(x)) → S(minus(x))
*1(s(x), y) → *1(x, y)
*1(p(x), y) → MINUS(y)
p(s(x)) → x
s(p(x)) → x
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
+1(p(x), y) → +1(x, y)
+1(p(x), y) → P(+(x, y))
+1(s(x), y) → S(+(x, y))
*1(p(x), y) → +1(*(x, y), minus(y))
MINUS(p(x)) → MINUS(x)
*1(p(x), y) → *1(x, y)
MINUS(s(x)) → MINUS(x)
*1(s(x), y) → +1(*(x, y), y)
MINUS(s(x)) → P(minus(x))
+1(s(x), y) → +1(x, y)
MINUS(p(x)) → S(minus(x))
*1(s(x), y) → *1(x, y)
*1(p(x), y) → MINUS(y)
p(s(x)) → x
s(p(x)) → x
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
MINUS(p(x)) → MINUS(x)
MINUS(s(x)) → MINUS(x)
p(s(x)) → x
s(p(x)) → x
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINUS(p(x)) → MINUS(x)
MINUS(s(x)) → MINUS(x)
The value of delta used in the strict ordering is 1/4.
POL(MINUS(x1)) = (1/2)x_1
POL(p(x1)) = 9/4 + x_1
POL(s(x1)) = 1/2 + (3/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
p(s(x)) → x
s(p(x)) → x
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
+1(p(x), y) → +1(x, y)
+1(s(x), y) → +1(x, y)
p(s(x)) → x
s(p(x)) → x
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(p(x), y) → +1(x, y)
+1(s(x), y) → +1(x, y)
The value of delta used in the strict ordering is 1/4.
POL(p(x1)) = 1/2 + (3/2)x_1
POL(s(x1)) = 9/4 + x_1
POL(+1(x1, x2)) = (1/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
p(s(x)) → x
s(p(x)) → x
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
*1(p(x), y) → *1(x, y)
*1(s(x), y) → *1(x, y)
p(s(x)) → x
s(p(x)) → x
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
*1(p(x), y) → *1(x, y)
*1(s(x), y) → *1(x, y)
The value of delta used in the strict ordering is 1/4.
POL(*1(x1, x2)) = (1/2)x_1
POL(p(x1)) = 9/4 + x_1
POL(s(x1)) = 1/2 + (3/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
p(s(x)) → x
s(p(x)) → x
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))